k:, X:(), y:( List).
(k  ||y||)  (q-linear(k;j.X(j);y) = (q-linear(k - 1;j.X(j);y) + (X(k) * y[(k - 1)]))  ) 

latex

Definitions	, P & Q, x. t(x), False, A, t  T, True, T, P  Q, P  Q, x(s), q-linear(k;i.X(i);y), A  B, P  Q, , x:A. B(x), i  j < k, {i..j}, , S  T
Lemmas	qadd comm q, qadd ac 1 q, mon assoc q, qmul comm qrng, nat plus wf, nat wf, nat plus inc, qsum wf, int seg wf, length wf1, select wf, qmul wf, sum unroll hi q, le wf, rationals wf, true wf, squash wf, qadd wf